COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	Le programme BOYER est une version miniaturisee du fameux
C00005 ENDMK
C⊗;
Le programme BOYER est une version miniaturisee du fameux
programme de BOYER-MOORE.
Ya tout le tremblement: evaluation symbolique, induction struc-
turelle, generalisation, subst. de l'hypothese d'induction ...

Les commandes:
1) definitions de fonctions VLISP ordinaires (peuvent s'inter-appeller).
2) (ana ---le-nom-de-la-fonction---), quoter le nom SVP.
   suit obligatoirement la definition, si la fonction est
   utilisee dans un theoreme (ca ne l'empeche pas de tourner).
3) (theo ---partie-gauche---  =  ---partie-droite)
   pour soumettre le theoreme a l'interactiveteoremprouvere.
4) (induct list ---nom-de-variable---) , induction type-liste.
5) (induct num  ---nom-de-variable---) , itou sur type-nombre.
6) (gen ---expression-i---   ---var-i---  ...) pour i = 1,n
   substitue (generalisation) les expressions-i aux variables-i.
7) (indhyp n  ---direction---)
   substitue a la n-ieme occurence de la partie gauche 
   de l'hypothese d'induction (direction = ->) 
   sa partie gauche.
   L'inverse si direction = <- .

Exemple de session:
.do rvlisp boyer
	; On definit une fonction app ;
(de app (x y) (if (null x) y (cons (car x) (app (cdr x) y))))
	; On en demande une analyse succinte ;
(ana 'app)
	; On rentre le theoreme qu'on souhaite demontrer ;
(theo (app x (app y z)) = (app (app x y) z))
	; Faut faire une induction structurelle de type-liste
	  sur la variable x ;
(induct list x)
	; Faut utiliser l'hypothese d'induction en
	  substituant sa partie droite (->) a sa partie gauche,
	  et sur la 1ere occurence de la partie gauche;
(indhyp  1 ->)
	; Voila le theoreme demontre !!! ;


Que les primitives recursives soient avec vous.